Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(app(*,x),app(app(+,y),z))	→ app(app(+,app(app(,x),y)),app(app(,x),z))
2:		app(app(*,app(app(+,y),z)),x)	→ app(app(+,app(app(,x),y)),app(app(,x),z))
3:		app(app(,app(app(,x),y)),z)	→ app(app(,x),app(app(,y),z))
4:		app(app(+,app(app(+,x),y)),z)	→ app(app(+,x),app(app(+,y),z))

There are 15 dependency pairs:


5:		APP(app(*,x),app(app(+,y),z))	→ APP(app(+,app(app(,x),y)),app(app(,x),z))
6:		APP(app(*,x),app(app(+,y),z))	→ APP(+,app(app(*,x),y))
7:		APP(app(*,x),app(app(+,y),z))	→ APP(app(*,x),y)
8:		APP(app(*,x),app(app(+,y),z))	→ APP(app(*,x),z)
9:		APP(app(*,app(app(+,y),z)),x)	→ APP(app(+,app(app(,x),y)),app(app(,x),z))
10:		APP(app(*,app(app(+,y),z)),x)	→ APP(+,app(app(*,x),y))
11:		APP(app(*,app(app(+,y),z)),x)	→ APP(app(*,x),y)
12:		APP(app(*,app(app(+,y),z)),x)	→ APP(app(*,x),z)
13:		APP(app(*,app(app(+,y),z)),x)	→ APP(*,x)
14:		APP(app(,app(app(,x),y)),z)	→ APP(app(,x),app(app(,y),z))
15:		APP(app(,app(app(,x),y)),z)	→ APP(app(*,y),z)
16:		APP(app(,app(app(,x),y)),z)	→ APP(*,y)
17:		APP(app(+,app(app(+,x),y)),z)	→ APP(app(+,x),app(app(+,y),z))
18:		APP(app(+,app(app(+,x),y)),z)	→ APP(app(+,y),z)
19:		APP(app(+,app(app(+,x),y)),z)	→ APP(+,y)

The approximated dependency graph contains one SCC: {5,7-9,11,12,14,15,17,18}.

Consider the SCC {5,7-9,11,12,14,15,17,18}. By taking the AF π with π(app) = π(APP) = 1 together with the lexicographic path order with precedence * ≻ +, the rules in {3,4,7,8,11,12,14,15,17,18} are weakly decreasing and the rules in {1,2,5,9} are strictly decreasing. There is one new SCC.
- Consider the SCC {7,8,11,12,14,15,17,18}. The constraints could not be solved.

Tyrolean Termination Tool (0.17 seconds) --- May 4, 2006